(**
 * Yet another pretty printer
 * @author UENO Katsuhiro
 * @copyright (C) 2021 SML# Development Team.
 *)
structure PrettyPrinter2 : sig

  val format : {outputFn : (string -> unit) option, width : int}
               -> FormatExpression.expression list
               -> string

end =
struct

  datatype priority = datatype FormatExpression.priority
  datatype assocDirection = datatype FormatExpression.assocDirection
  datatype expression = datatype FormatExpression.expression

  type assoc =
      {strength : int, direction : assocDirection}

  fun leftAssoc ({direction = Right, strength}:assoc) : assoc =
      {direction = Neutral, strength = strength}
    | leftAssoc a = a

  fun rightAssoc ({direction = Left, strength}:assoc) : assoc =
      {direction = Neutral, strength = strength}
    | rightAssoc a = a

  fun isWeakerThanOrEqualTo ({strength = s1, direction = d1}:assoc,
                             {strength = s2, direction = d2}:assoc) =
      (* as defined in OVERVIEW_ja.txt *)
      s1 < s2 orelse case (d1, d2) of
                       (Left, Neutral) => s1 <= s2
                     | (Right, Neutral) => s1 <= s2
                     | _ => d1 = d2 andalso s1 = s2

  datatype text =
      STRING of string
    | SPACE of int
    | NEWLINE

  type output =
      {outputFn : (string -> unit) option,
       buffer : text list,  (* reverse order *)
       column : int,
       width : int}

  fun canPut ({column, width, ...}:output) len =
      column + len <= width

  fun putString ({outputFn, buffer, column, width}:output) len string : output =
      {outputFn = outputFn,
       buffer = case string of "" => buffer | _ => STRING string :: buffer,
       column = column + len,
       width = width}

  fun putSpace (output as {outputFn, buffer, column, width}:output) count =
      if count > 0
      then {outputFn = outputFn,
            buffer = SPACE count :: buffer,
            column = column + count,
            width = width}
      else output

  fun putNewline ({outputFn, buffer, column, width}:output) =
      {outputFn = outputFn,
       buffer = NEWLINE :: buffer,
       column = 0,
       width = width}

  fun whiteSpaces n =
      CharVector.tabulate (n, fn _ => #" ")

  fun getLineBody z (STRING x :: t) = getLineBody (x :: z) t
    | getLineBody z (SPACE n :: t) = getLineBody (whiteSpaces n :: z) t
    | getLineBody z l = (z, l)

  fun getLine z (NEWLINE :: t) = getLine ("\n" :: z) t
    | getLine z (SPACE _ :: t) = getLine z t
    | getLine z l = getLineBody z l

  fun getLines z texts =
      case getLine z texts of
        (z, nil) => z
      | (z, rest) => getLines z rest
  val getLines = fn texts => getLines nil texts

  fun commit outputFn z nil = app outputFn z
    | commit outputFn z texts =
      case getLine nil texts of
        (nil, rest) => commit outputFn z rest
      | (strings, rest) => commit outputFn (String.concat strings :: z) rest
  val commit = fn outputFn => fn texts => commit outputFn nil texts

  fun dump (output as {outputFn = NONE, ...}:output) = output
    | dump {outputFn as SOME f, buffer, column, width} =
      (commit f buffer;
       {outputFn = outputFn,
        buffer = nil,
        column = column,
        width = width})

  type indent =
      {level : int, indents : int list}

  (**
   * the context of nested guards.  
   *)
  datatype context =
      (**
       * in a guard.
       * @params {base, nest, priority}
       * @param base       the number of outermost guards ignored.
       * @param nest       the nest level of the current guard.
       *                   'nest' must be bigger than or equal to 'base'.
       * @param priority   the lowest priority for indicators to be linebreak.
       *)
      GUARD of {base : int, nest : int, priority : int}
    | (**
       * not in a guard, or in a guard whose preferred indicators have all
       * become linebreaks.
       * @params base
       * @param base       the number of outer guards ignored.
       *)
      TOP of int

  (**
   * pending input of the pretty printer machine.
   *)
  datatype next =
      (** pending input and its associativity *)
      NEXT of expression list * assoc
    | (** the end of guards *)
      DELIM of indent

  (**
   * the priority of restarts.
   *)
  datatype priority =
      (**
       * generated by a preferred indicator.
       * @params (nest, priority)
       * @param nest       the nest level of the indicator
       * @param priority   the priority of the indicator
       *)
      PREFERRED of int * int
    | (**
       * generated by a deferred indicator.
       *)
      DEFERRED

  (**
   * restart: the continuation of backtracking.
   *)
  datatype restart =
      (** no restart exists *)
      NORESTART
    | (**
       * a restart exists.
       * RESTART may be nested through 'state'.
       * The outer restart must have higher 'priority' than the inner one.
       * @params {priority, outoput, state}
       * @param priority   the priority of the restart
       * @param output     the restart output
       * @param state      the restart state
       *)
      RESTART of {priority : priority, output : output, state : state}

  (**
   * the state of the pretty printer machine.
   * @params {input, indent, assoc, next, restart, context}
   * @param input          the sequence to be interpreted
   * @param indent         current indent
   * @param assoc          current associativity
   * @param next           the sequence of pending inputs
   * @param restart        the most-preceded restart currently available
   * @param context        current context of nested guards
   *)
  withtype state =
    {input : expression list,
     indent : indent,
     assoc : assoc,
     next : next list,
     restart : restart,
     context : context}

  fun precedesTo (DEFERRED, DEFERRED) = true
    | precedesTo (DEFERRED, PREFERRED _) = false
    | precedesTo (PREFERRED _, DEFERRED) = true
    | precedesTo (PREFERRED (n1, p1), PREFERRED (n2, p2)) =
      n1 < n2 orelse (n1 = n2 andalso p1 < p2)

  fun precedesToRestart (_, NORESTART) = true
    | precedesToRestart (newPriority, RESTART {priority, ...}) =
      precedesTo (newPriority, priority)

  fun run (output : output)
          ({input = nil,
           indent = _,
           assoc,
           next = DELIM indent :: next,
           restart,
           context} : state) =
      run output
          {input = nil,
           indent = indent,
           assoc = assoc,
           next = next,
           restart = restart,
           context =
             case context of
               GUARD {base, nest, priority} =>
               if base = nest
               then TOP base
               else GUARD {base = base,
                           nest = nest - 1,
                           priority = priority}
             | TOP nest => if nest > 0 then TOP (nest - 1) else context}

    | run output {input = nil, next = nil, ...} =
      String.concat (getLines (#buffer (dump output)))

    | run output
          {input = nil,
           indent,
           assoc = _,
           next = NEXT (input, assoc) :: next,
           restart,
           context} =
      run output
          {input = input,
           indent = indent,
           assoc = assoc,
           next = next,
           restart = restart,
           context = context}

    | run output
          {input = Sequence nil :: input,
           indent,
           assoc,
           next,
           restart,
           context} =
      run output
          {input = input,
           indent = indent,
           assoc = assoc,
           next = next,
           restart = restart,
           context = context}

    | run output
          {input = Sequence newInput :: nil,
           indent,
           assoc,
           next,
           restart,
           context} =
      run output
          {input = newInput,
           indent = indent,
           assoc = assoc,
           next = next,
           restart = restart,
           context = context}

    | run output
          {input = Sequence newInput :: input,
           indent,
           assoc,
           next,
           restart,
           context} =
      run output
          {input = newInput,
           indent = indent,
           assoc = case input of [EndOfIndent] => assoc | _ => leftAssoc assoc,
           next = NEXT (input, rightAssoc assoc) :: next,
           restart = restart,
           context = context}

    | run output
          {input = StartOfIndent n :: input,
           indent = {level, indents},
           assoc,
           next,
           restart,
           context} =
      run output
          {input = input,
           indent = {level = level + n, indents = n :: indents},
           assoc = assoc,
           next = next,
           restart = restart,
           context = context}

    | run output
          {input = EndOfIndent :: input,
           indent as {level, indents},
           assoc,
           next,
           restart,
           context} =
      run output
          {input = input,
           indent =
             case indents of
               n :: indents => {level = level - n, indents = indents}
             | nil => indent,
           assoc = assoc,
           next = next,
           restart = restart,
           context = context}

    | run output
          {input = Guard (SOME {cut, strength, direction}, body) :: input,
           indent,
           assoc,
           next,
           restart,
           context} =
      let
        val innerAssoc = {strength = strength, direction = direction}
        val outerAssoc = case input of nil => assoc | _::_ => leftAssoc assoc
      in
        if cut orelse isWeakerThanOrEqualTo (outerAssoc, innerAssoc)
        then run output
                 {input = [Guard (NONE, body)],
                  indent = indent,
                  assoc = innerAssoc,
                  next = NEXT (input, rightAssoc assoc) :: next,
                  restart = restart,
                  context = context}
        else run output
                 {input = Term (1, "(") :: nil,
                  indent = indent,
                  assoc = outerAssoc,
                  next =
                    NEXT ([Guard (NONE, body)], innerAssoc)
                    :: NEXT (Term (1, ")") :: input, rightAssoc assoc)
                    :: next,
                  restart = restart,
                  context = context}
      end

    | run (output as {column, ...})
          {input = Guard (NONE, body) :: input,
           indent,
           assoc,
           next,
           restart,
           context} =
      run output
          {input = body,
           indent = {level = column, indents = nil},
           assoc = case input of nil => assoc | _::_ => leftAssoc assoc,
           next = DELIM indent :: NEXT (input, rightAssoc assoc) :: next,
           restart = restart,
           context =
             case context of
               TOP n => GUARD {base = n, nest = n, priority = 0}
             | GUARD {base, nest, priority} =>
               GUARD {base = base, nest = nest + 1, priority = priority}}

    | run output
          {input = Indicator {space, newline = SOME {priority = Preferred n}}
                   :: input,
           indent,
           assoc,
           next,
           restart,
           context as TOP _} =
      run output
          {input = Newline :: input,
           indent = indent,
           assoc = assoc,
           next = next,
           restart = restart,
           context = context}

    | run output
          {input = Indicator {space, newline = SOME {priority = Preferred n}}
                   :: input,
           indent,
           assoc,
           next,
           restart,
           context as GUARD {base, nest, priority}} =
      if nest = base andalso n <= priority
      then run output
               {input = Newline :: input,
                indent = indent,
                assoc = assoc,
                next = next,
                restart = restart,
                context = context}
      else run output
               {input = if space then Term (1, " ") :: input else input,
                indent = indent,
                assoc = assoc,
                next = next,
                restart =
                  if precedesToRestart (PREFERRED (nest, n), restart)
                  then RESTART {priority = PREFERRED (nest, n),
                                output = output,
                                state = {input = Newline :: input,
                                         indent = indent,
                                         assoc = assoc,
                                         next = next,
                                         restart = restart,
                                         context = GUARD {base = nest,
                                                          nest = nest,
                                                          priority = n}}}
                  else restart,
                context = context}

    | run output
          {input = Indicator {space, newline = SOME {priority = Deferred}}
                   :: input,
           indent,
           assoc,
           next,
           restart,
           context} =
      run output
          {input = if space then Term (1, " ") :: input else input,
           indent = indent,
           assoc = assoc,
           next = next,
           restart =
             if precedesToRestart (DEFERRED, restart)
             then RESTART {priority = DEFERRED,
                           output = output,
                           state = {input = Newline :: input,
                                    indent = indent,
                                    assoc = assoc,
                                    next = next,
                                    restart = restart,
                                    context = case context of
                                                TOP base => context
                                              | GUARD {nest, ...} => TOP nest}}
             else restart,
           context = context}

    | run output
          {input = Indicator {space, newline = NONE} :: input,
           indent,
           assoc,
           next,
           restart,
           context} =
      run output
          {input = if space then Term (1, " ") :: input else input,
           indent = indent,
           assoc = assoc,
           next = next,
           restart = restart,
           context = context}

    | run output
          {input = Newline :: input,
           indent as {level, ...},
           assoc,
           next,
           restart,
           context} =
      let
        val newRestart =
            case context of
              TOP _ => NORESTART
            | GUARD {base, nest, priority} =>
              case restart of
                RESTART {priority = DEFERRED, ...} => NORESTART
              | RESTART {priority = PREFERRED (nest, _), ...} =>
                if nest > base then NORESTART else restart
              | _ => restart
      in
        run (case newRestart of
               NORESTART => putSpace (dump (putNewline output)) level
             | RESTART _ => putSpace (putNewline output) level)
            {input = input,
             indent = indent,
             assoc = rightAssoc assoc,
             next = next,
             restart = newRestart,
             context = context}
      end

    | run output
          {input = Term (len, string) :: input,
           indent,
           assoc,
           next,
           restart,
           context} =
      if canPut output len
      then run (putString output len string)
               {input = input,
                indent = indent,
                assoc = rightAssoc assoc,
                next = next,
                restart = restart,
                context = context}
      else case restart of
             RESTART {output, state, priority} => run output state
           | NORESTART =>
             run (putString output len string)
                 {input = input,
                  indent = indent,
                  assoc = rightAssoc assoc,
                  next = next,
                  restart = NORESTART,
                  context = case context of
                              TOP _ => context
                            | GUARD {nest, ...} => TOP nest}

  fun format {outputFn, width} expressions =
      run {outputFn = outputFn,
           buffer = nil,
           column = 0,
           width = width}
          {input = [Guard (NONE, expressions)],
           indent = {level = 0, indents = nil},
           assoc = {strength = 0, direction = Neutral},
           next = nil,
           restart = NORESTART,
           context = TOP 0}

end
